Trace Monad refactor #664

corlewis · 2023-08-14T08:50:09Z

This PR refactors the Trace Monad to have the same general structure and style as the Nondet Monad. In particular:

the main Trace_Monad file now only contains the basic monad definitions and lemmas about them
other definitions (like valid, validI, no_fail, no_trace, etc.) and their lemmas are in their own files.

The intentions for the commits in this PR and the reviewing suggestions are as follows:

the first commit updates style and content to match Nondet Monad's and hopefully just needs minimal review
the second moves content that also appears in Nondet Monad to match the structure of Nondet Monad and hopefully just needs minimal review
the third moves content specific to the Trace Monad to different files and hopefully just needs the new locations reviewed
the fourth makes changes to the content specific to the Trace Monad and should be reviewed as normal
the fifth updates the rest of lib as needed and should be reviewed as normal.

lib/Monads/trace/Trace_Monad.thy

Xaphiosis · 2023-08-15T06:59:53Z

lib/Monads/trace/Trace_Monad.thy

+  The following two instantiations are convenient to separate reasoning for exceptional and
+  normal case.\<close>
+(* Narrator: they are in fact not convenient, and are now considered a mistake that should have
+             been an abbreviation instead. *)


does this indicate this should be a FIXME?

Maybe? This comment is copied verbatim from the nondet monad though, so I'd prefer not to change it as part of this work.

FIXME would indicate intent to change it. I think we probably don't want to change this, but we should also record that it probably wasn't the optimal decision to go with this in the first place.

To clarify, there actually is a FIXME on the definition in the following line, saying (* FIXME lib: this should be an abbreviation *)
See https://github.com/seL4/l4v/blob/master/lib/Monads/nondet/Nondet_VCG.thy#L66

lib/Monads/trace/Trace_Monad.thy

lib/Monads/trace/Trace_VCG.thy

Xaphiosis · 2023-08-15T07:12:13Z

lib/Monads/trace/Trace_Monad.thy

@@ -645,7 +653,8 @@ subsection "Loops"
 text \<open>
  Loops are handled using the following inductive predicate;
  non-termination is represented using the failure flag of the
-  monad.\<close>
+  monad.
+FIXME: update comment about non-termination\<close>


was this FIXME intended to be left in?

Sort of, or at least it still needs to be updated. I'll either need to stare at this more to work out how non-termination is represented here or get help from someone who understands better how these loops are constructed.

We should leave the FIXME in. I don't think we have properly thought about how this should be defined yet. In particular, in the concurrent setting it does make sense to have a semantics for non-terminating loops, so the whole definition here might have to be rethought (or maybe a potentially non-terminating loop should get a separate definition).

Xaphiosis · 2023-08-15T07:16:26Z

lib/Monads/trace/Trace_RG.thy

  apply (subst prefix_closed_def, clarsimp simp: bind_def)
  apply (auto simp: Cons_eq_append_conv split: tmres.split_asm
             dest!: prefix_closedD[rotated];
-    fastforce elim: rev_bexI)
+         fastforce elim: rev_bexI)


this indent doesn't seem right

The indent seems right to me, but the auto ...; fastforce method is obviously terrible. I'll see if I can rework it into something nicer.

The fastforce is to the left of the (, which can't be right. The dest!: on the auto should align with the simp, not the auto, and then the fastforce goes after the semicolon, so should be on the same level as the auto.
NEVER MIND: this is an error between chair and keyboard, commit-by-commit reviews for large cleanups like this are difficult it seems.
That said, I agree with the method itself being terrible, but can deal with it another time.

Also happy to leave this one for later, yes.

lib/Monads/trace/Trace_Det.thy

lib/Monads/trace/Trace_In_Monad.thy

Xaphiosis · 2023-08-15T07:26:45Z

For commit messages, there are some that refer to trace as a thing on its own, e.g. trace files, but other commits say trace monad. Would it be possible to have trace monad in all cases? For example, I find lib: update for trace refactor confusing

lib/Monads/trace/Trace_Strengthen_Setup.thy

lib/Monads/trace/Trace_No_Throw.thy

lib/Monads/trace/Trace_Monad_Equations.thy

Xaphiosis

This is a superb overhaul of the mess we had before, and you were way more thorough than I thought anyone would have the energy for. Many thanks and words of praise!

It's also a huge diff, so it was difficult to review. I didn't see anything moved to somewhere where it shouldn't have been. I had a few things I noticed or had questions about, but even if this goes in as-is it's a huge improvement. Further improvements should be incremental after this PR goes in, especially when we get to finally using the trace monad in more developments.

corlewis · 2023-08-16T03:01:47Z

For commit messages, there are some that refer to trace as a thing on its own, e.g. trace files, but other commits say trace monad. Would it be possible to have trace monad in all cases? For example, I find lib: update for trace refactor confusing

Good point, I'll try to make that consistent.

corlewis · 2023-08-18T06:48:59Z

The last force push did involve some new changes, but they were just restyling the theory imports to be consistent and hopefully aren't controversial.

lsf37

Nice work!

We might have this somewhere already and I missed it: do we have a lemma that shows that the Hoare triples are equivalent to RG-statements with R=G=UNIV? (Or is that not true?) If it is true, that's something we should probably add, which then leads to the question if triples should be an abbreviation. All of that is for another PR, looking through this material just made me think of the connection.

lib/Monads/trace/Trace_Monad.thy

lsf37 · 2023-08-18T09:27:27Z

lib/Monads/trace/Trace_Monad.thy

@@ -645,7 +653,8 @@ subsection "Loops"
 text \<open>
  Loops are handled using the following inductive predicate;
  non-termination is represented using the failure flag of the
-  monad.\<close>
+  monad.
+FIXME: update comment about non-termination\<close>


We should leave the FIXME in. I don't think we have properly thought about how this should be defined yet. In particular, in the concurrent setting it does make sense to have a semantics for non-terminating loops, so the whole definition here might have to be rethought (or maybe a potentially non-terminating loop should get a separate definition).

lsf37 · 2023-08-18T09:29:17Z

lib/Monads/trace/Trace_RG.thy

  apply (subst prefix_closed_def, clarsimp simp: bind_def)
  apply (auto simp: Cons_eq_append_conv split: tmres.split_asm
             dest!: prefix_closedD[rotated];
-    fastforce elim: rev_bexI)
+         fastforce elim: rev_bexI)


Also happy to leave this one for later, yes.

lsf37 · 2023-08-18T09:33:42Z

lib/Monads/trace/Trace_Monad.thy

+  The following two instantiations are convenient to separate reasoning for exceptional and
+  normal case.\<close>
+(* Narrator: they are in fact not convenient, and are now considered a mistake that should have
+             been an abbreviation instead. *)


FIXME would indicate intent to change it. I think we probably don't want to change this, but we should also record that it probably wasn't the optimal decision to go with this in the first place.

corlewis · 2023-08-21T02:00:28Z

We might have this somewhere already and I missed it: do we have a lemma that shows that the Hoare triples are equivalent to RG-statements with R=G=UNIV? (Or is that not true?) If it is true, that's something we should probably add, which then leads to the question if triples should be an abbreviation. All of that is for another PR, looking through this material just made me think of the connection.

Good idea, I don't think we have something like that yet. I'll see if it's easy to prove, and if it is then I'll add it in the next PR.

This should now be in sync with Nondet_Monad.thy wherever the two files have similar content. Signed-off-by: Corey Lewis <[email protected]>

This splits material out of Trace_Monad and Trace_VCG and into more specific theories, following the same approach and structure as the nondet theories. This commit is mainly focused on definitions and lemmas that also appear in the nondet monad; trace monad concepts are left where they are for now. Signed-off-by: Corey Lewis <[email protected]>

Signed-off-by: Corey Lewis <[email protected]>

corlewis added the multicore anything related to multicore verification label Aug 14, 2023

corlewis requested review from Xaphiosis and lsf37 August 14, 2023 08:50

corlewis self-assigned this Aug 14, 2023

corlewis mentioned this pull request Aug 14, 2023

Minor Nondet Monad improvements #665

Merged

corlewis added the cleanup label Aug 14, 2023

corlewis force-pushed the trace_refactor branch 3 times, most recently from aa3ec99 to e3dde74 Compare August 15, 2023 03:10